%\newpage
As argued along the paper, a main contribution of this work is the extension of session types disciplines with a simple notion of \emph{interface}.
Using interfaces, we are able to give
simple and intuitive typing rules for located and update processes---see rules \rulename{t:Loc} and \rulename{t:Adapt} in Table~\ref{tab:ts}.
It is thus legitimate to investigate how to enhance the notion of interface and its associated definitions.
Here we discuss a few alternatives.  
The discussion is kept brief and informal: our aim is to illustrate how the presented framework already provides
a basis for more sophisticated analyses---a formal treatment of these ideas is out of the scope of this paper and is left for future work.

A straightforward enhancement concerns 
the typing of adaptable processes. Consider 
the following alternative  formulation for typing rule \rulename{t:Adapt}:
$$
\cfrac{\Theta \vdash l:\INT_1  \qquad  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT_1}}}{P}{\type{\emptyset}{ \INT_2 }}  \qquad \boxed{~\INT_1 \intpr \INT_2~}}{\judgebis{\env{\Gamma}{\Theta}}{\adapt{l}{P}{X}}{\type{\emptyset}{ \emptyset}}} \quad \rulename{t:MonAdapt}  \vspace{2mm}
$$
Clearly, the above rule  is more restrictive than \rulename{t:Adapt}, i.e., it accepts less update processes as typable. 
Still, this rule captures a requirement that may be desirable in several contexts, namely that 
the behavior after adaptation is ``at least'' the behavior offered before, possibly adding new behaviors.
Indeed, by disallowing adaptation routines that discard behavior, rule \rulename{t:MonAdapt} is suitable 
to reason about settings in which adaptation/upgrade actions need to be tightly controlled. 





% and the typing rule 

\begin{table}[!t]
%{\small
\begin{eqnarray*}
&
\inferrule[\rulename{s:End}]{ }{\epsilon \subt \epsilon} 
\qquad
\inferrule[\rulename{s:InE} ]{\forall i.(\tau_i ~ \subt ~\sigma_i)  \qquad \alpha_1 ~ \subt ~\alpha_2 }{?(\tilde{\tau}).\alpha_1 ~ \subt~ ?(\tilde{\sigma}).\alpha_2} 
\qquad
\inferrule[\rulename{s:InC}]{\beta_1 ~ \subt ~\beta_2  \qquad \alpha_1 ~ \subt ~\alpha_2 }{?(\beta_1).\alpha_1 ~ \subt ~?(\beta_2).\alpha_2} 
\quad  
&
 \\  
&
\inferrule[\rulename{s:OutE}]{\forall i.(\tau_i ~ \subt ~\sigma_i)  \qquad \alpha_1 ~ \subt ~\alpha_2 }{!(\tilde{\sigma}).\alpha_1 ~ \subt ~ !(\tilde{\tau}).\alpha_2} 
\qquad
\inferrule[\rulename{s:OutC} ]{\beta_1 ~ \subt ~\beta_2  \qquad \alpha_1 ~ \subt ~\alpha_2 }{!(\beta_2).\alpha_1 ~ \subt ~!(\beta_1).\alpha_2} 
&
\\
&
\inferrule[\rulename{s:Branch}]{\forall i \in \{1, \ldots, m\}. \alpha_i \subt \beta_i}{\&\{n_1:\alpha_1,\ldots, n_m:\alpha_m \} ~ \subt ~ \&\{n_1:\beta_1,\ldots, n_{m+j}:\beta_{m+j} \} } 
\quad  
&
 \\
 &
\inferrule[\rulename{s:Choice}]{\forall i \in \{1, \ldots, m\}. \alpha_i \subt \beta_i}{\oplus\{n_1:\alpha_1,\ldots, n_{m+j}:\alpha_{m+j} \} ~ \subt ~ \oplus\{n_1:\beta_1,\ldots, n_m:\beta_{m} \} } 
& 
\end{eqnarray*}
\caption{Subtyping rules. 
Intuitively, $\alpha \subt \beta$ is read as:
any process of type $\alpha$ can safely be used in a context where a process of type $\beta$ is expected.
} \label{tab:subt}
\end{table}

In the context of more stringent typing rules such as \rulename{t:MonAdapt}, it is convenient to find ways for relaxing the 
interface preorder \intpr in Def.~\ref{d:intpre}. 
As this preorder is central to our approach for disciplined runtime adaptation, 
a relaxed definition for it
may  lead to more flexible typing disciplines.
One alternative is to rely on
\emph{subtyping} for session types for such a relaxed definition.
We briefly recall the essential features of subtyping in session types; see~\cite{DBLP:journals/acta/GayH05,DBLP:journals/fuin/VallecilloVR06} for details. 
Given types $\alpha, \beta$, we say that 
$\alpha$ is a \emph{subtype} of $\beta$ (noted $\alpha \subt \beta$) 
if, 
intuitively, 
any process of type $\alpha$ can safely be used in a context where a process of type $\beta$ is expected. 
On basic types, subtyping arises from subset relations (as in, e.g., $\mathsf{int} \subt \mathsf{real}$).
For session types, $\subt$ is defined by the rules in Table~\ref{tab:subt}.
Observe how  $\subt$ is co-variant for input prefixes and contra-variant for outputs, 
whereas it is co-variant for branching and contra-variant for choices.

By relying on $\subt$, it is possible to define a more flexible preorder over interfaces:
\begin{definition}[Refined Interface Preorder] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr_\text{sub} \INT'$ iff 
\begin{enumerate}[1.]
\item $\INT_\quau \subseteq \INT'_\quau$ and $\forall \inter{a}{\alpha}{h} \in \INT_\quau. \exists \inter{a}{\beta}{h} \in \INT'_\quau$ such that $\alpha \subt \beta$.
\item $\forall \inter{a}{\alpha}{h} \in \INT_\qual $  then 
$ \inter{a}{\beta}{h'} \in \INT'_\qual $, such that  $\alpha \subt \beta$ and \\ $h \leq h'$, for some $h'$.
\end{enumerate}
\end{definition}

It is immediate to see how $\intpr_\text{sub}$ improves over $\intpr$ by 
offering a more flexible and fine-grained relation over interfaces, in which subtyping replaces strict type equality.
We conjecture our main results (Theorems~\ref{t:safety} and \ref{t:consist}) 
would also hold, with little modifications, for the modified typing system 
that results by replacing 
\rulename{t:Adapt} with rule \rulename{t:MonAdapt} above, and by replacing \intpr  with $\intpr_\text{sub}$
in the appropriate places in Table~\ref{tab:ts}, 
Lemma~\ref{lem:substitution}(3), and Theorem~\ref{th:subred}.
% and \ref{tab:session}.
